This example introduces a simple token contract, allowing users to transfer tokens to each other.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;
contract BasicToken {
mapping(address => uint) public balances;
constructor(uint initialSupply) {
balances[msg.sender] = initialSupply;
}
function transfer(address recipient, uint amount) public {
require(balances[msg.sender] >= amount, "Insufficient balance");
balances[msg.sender] -= amount;
balances[recipient] += amount;
}
}
In this contract:
transfer function allows users to send tokens to another address, as long as they have enough balance.module BASIC-TOKEN // Defines the module name "BASIC-TOKEN".
imports INT // Imports the INT module to use integer operations.
imports MAP // Imports the MAP module to use mappings (key-value pairs).
imports BOOL // Imports the BOOL module to use boolean expressions.
syntax TokenAction ::= "transfer" // Defines a syntax for a TokenAction, with "transfer" as an action.
syntax Address ::= String // Defines Address type as a string to represent user addresses.
syntax TokenState ::= Map // Defines TokenState as a Map to represent the token balances.
syntax KResult ::= Int // Defines KResult as an integer, which can be the result type in K operations.
configuration <k> $PGM:K </k> // Defines the K configuration with a program component $PGM of type K.
<balances> .Map </balances> // Defines the balances component as a map to store each address's token balance.
// Rule for token transfer
rule <k> transfer => . ... </k> // Starts defining the "transfer" rule in the program (K) context.
<balances> (SENDER |-> BAL) => // Accesses the sender's balance (BAL) in the balances map.
(SENDER |-> BAL - AMOUNT) ... // Updates the sender's balance to subtract the transferred amount.
(RECIPIENT |-> RBAL) => // Accesses the recipient's balance (RBAL) in the balances map.
(RECIPIENT |-> RBAL + AMOUNT) // Updates the recipient's balance to add the transferred amount.
</balances> // Closes the balances component update.
requires BAL >=Int AMOUNT // Ensures that the sender has enough tokens for the transfer.
This specification:
transfer rule only applies if the sender has enough tokens (BAL >= AMOUNT).This example introduces a counter contract where only the owner can increment or decrement the counter.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;
contract Counter {
address public owner;
int public count;
constructor() {
owner = msg.sender;
count = 0;
}
modifier onlyOwner() {
require(msg.sender == owner, "Not the owner");
_;
}
function increment() public onlyOwner {
count += 1;
}
function decrement() public onlyOwner {
count -= 1;
}
}
In this contract:
onlyOwner modifier ensures that only the contract owner can call increment and decrement.increment and decrement functions modify the counter.module COUNTER // Defines the module named "COUNTER".
imports INT // Imports the INT module to use integer operations.
imports BOOL // Imports the BOOL module to use boolean expressions.
syntax CounterAction ::= "increment" | "decrement" // Defines CounterAction with two possible actions: "increment" and "decrement".
syntax Address ::= String // Defines Address type as a String to represent user addresses.
syntax CounterState ::= Int // Defines CounterState as an integer type for the counter value.
syntax KResult ::= Int // Defines KResult as an integer, representing possible return values in K operations.
configuration <k> $PGM:K </k> // Defines the main program configuration component ($PGM) of type K.
<owner> .String </owner> // Defines the "owner" component as a string, representing the owner's address.
<count> 0 </count> // Defines the "count" component, initialized to 0, representing the counter value.
// Rule for increment function
rule <k> increment => . ... </k> // Begins the rule for the "increment" action in the program (K) context.
<count> CNT => CNT + 1 </count> // Updates the "count" value by incrementing it by 1.
requires SENDER == OWNER // Specifies a condition that the increment action only occurs if SENDER equals OWNER.
// Rule for decrement function
rule <k> decrement => . ... </k> // Begins the rule for the "decrement" action in the program (K) context.
<count> CNT => CNT - 1 </count> // Updates the "count" value by decrementing it by 1.
requires SENDER == OWNER // Specifies a condition that the decrement action only occurs if SENDER equals OWNER.
In this K specification:
increment and decrement rules require that the sender (SENDER) is the owner (OWNER) before modifying count.This example introduces a contract that adds two numbers and ensures the result doesn’t overflow.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;
contract SafeMath {
function safeAdd(uint a, uint b) public pure returns (uint) {
require(a + b >= a, "Addition overflow");
return a + b;
}
}
In this contract:
safeAdd function adds two unsigned integers and checks for overflow using a require statement.module SAFE-MATH // Defines the module named "SAFE-MATH".
imports INT // Imports the INT module to use integer operations.
syntax MathAction ::= "safeAdd" // Defines MathAction with one possible action: "safeAdd".
syntax KResult ::= Int // Defines KResult as an integer, representing the result type in K operations.
configuration <k> $PGM:K </k> // Defines the main configuration component ($PGM) of type K.
// Rule for safeAdd function
rule <k> safeAdd(A, B) => (A +Int B) ... </k> // Defines the "safeAdd" function rule in the program (K) context.
requires (A +Int B) >=Int A // Specifies a condition that ensures no overflow: the result must be greater than or equal to A.
In this K specification:
safeAdd rule only proceeds if the sum of A and B is greater than or equal to A, ensuring no overflow occurs.This example builds on the Simple Bank example, but only allows certain users to deposit and withdraw funds.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;
contract RestrictedBank {
address public admin;
mapping(address => uint) public balances;
constructor() {
admin = msg.sender;
}
modifier onlyAdmin() {
require(msg.sender == admin, "Not an admin");
_;
}
function deposit() public payable onlyAdmin {
balances[msg.sender] += msg.value;
}
function withdraw(uint amount) public onlyAdmin {
require(balances[msg.sender] >= amount, "Insufficient balance");
balances[msg.sender] -= amount;
payable(msg.sender).transfer(amount);
}
}
In this contract:
deposit and withdraw.module RESTRICTED-BANK // Defines the module named "RESTRICTED-BANK".
imports INT // Imports the INT module to use integer operations.
imports BOOL // Imports the BOOL module to use boolean expressions.
imports MAP // Imports the MAP module to use mappings (key-value pairs).
syntax BankAction ::= "deposit" | "withdraw" // Defines BankAction with two possible actions: "deposit" and "withdraw".
syntax Address ::= String // Defines Address type as a String to represent user addresses.
syntax BankState ::= Map // Defines BankState as a Map to represent account balances.
syntax KResult ::= Int // Defines KResult as an integer type for possible result values in K operations.
configuration <k> $PGM:K </k> // Defines the main configuration component ($PGM) of type K.
<admin> .String </admin> // Defines the "admin" component as a string, representing the administrator's address.
<balances> .Map </balances> // Defines the "balances" component as a map to store account balances.
// Rule for deposit function
rule <k> deposit => . ... </k> // Begins the rule for the "deposit" action in the program (K) context.
<balances> BALS => BALS[ADMIN <- BALS[ADMIN] + AMOUNT] </balances> // Updates the admin's balance by adding the deposit amount.
requires SENDER == ADMIN andBool AMOUNT >Int 0 // Specifies conditions: only the admin can deposit, and amount must be greater than zero.
// Rule for withdraw function
rule <k> withdraw => . ... </k> // Begins the rule for the "withdraw" action in the program (K) context.
<balances> (ADMIN |-> BAL) => (ADMIN |-> BAL - AMOUNT) </balances> // Updates the admin's balance by subtracting the withdrawal amount.
requires SENDER == ADMIN andBool BAL >=Int AMOUNT // Specifies conditions: only the admin can withdraw, and there must be sufficient balance.
In this K specification:
deposit and withdraw rules are restricted to the ADMIN.withdraw rule also checks for sufficient balance.This contract introduces a time-based lock mechanism where funds deposited by a user can only be withdrawn after a specific time period.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;
contract TimedLock {
struct Lock {
uint amount;
uint releaseTime;
}
mapping(address => Lock) public locks;
function deposit(uint timeInSeconds) public payable {
require(msg.value > 0, "No Ether sent");
locks[msg.sender] = Lock(msg.value, block.timestamp + timeInSeconds);
}
function withdraw() public {
Lock memory userLock = locks[msg.sender];
require(block.timestamp >= userLock.releaseTime, "Funds are locked");
require(userLock.amount > 0, "No funds to withdraw");
uint amount = userLock.amount;
locks[msg.sender].amount = 0;
payable(msg.sender).transfer(amount);
}
}
In this contract:
module TIMED-LOCK // Defines the module named "TIMED-LOCK".
imports INT // Imports the INT module to use integer operations.
imports MAP // Imports the MAP module to use mappings (key-value pairs).
imports BOOL // Imports the BOOL module to use boolean expressions.
syntax LockAction ::= "deposit" | "withdraw" // Defines LockAction with two possible actions: "deposit" and "withdraw".
syntax Address ::= String // Defines Address type as a String to represent user addresses.
syntax LockState ::= Map // Defines LockState as a Map to store lock data (e.g., amounts, release times).
syntax KResult ::= Int // Defines KResult as an integer, which can be the result type in K operations.
configuration <k> $PGM:K </k> // Defines the main configuration component ($PGM) of type K.
<locks> .Map </locks> // Defines the "locks" component as a map to store each address’s locked funds and release time.
<currentTime> 0 </currentTime> // Defines "currentTime" for simulating time in the module.
// Rule for deposit function
rule <k> deposit(TIME) => . ... </k> // Begins the rule for the "deposit" action.
<locks> LOCKS => LOCKS[ADDR <- { amount: AMOUNT, // Adds a lock for the depositor's address in the "locks" map.
releaseTime: (currentTime +Int TIME) }] </locks> // Sets the release time based on the deposit time.
requires AMOUNT >Int 0 // Ensures the deposit amount is greater than zero.
// Rule for withdraw function
rule <k> withdraw => . ... </k> // Begins the rule for the "withdraw" action.
<locks> LOCKS => LOCKS[ADDR <- { amount: 0, releaseTime: RELEASE }] </locks> // Sets the locked amount to zero after withdrawal.
requires LOCKS[ADDR].releaseTime <=Int currentTime // Ensures the current time has passed the release time.
andBool LOCKS[ADDR].amount >Int 0 // Ensures there are funds available to withdraw.
In this K specification:
deposit rule creates a lock with an amount and release time.withdraw rule ensures that funds are only withdrawn after the release time and updates the balance to zero after withdrawal.This example demonstrates a contract that manages a two-step approval process for transactions.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;
contract MultiStepApproval {
enum State { Initiated, Approved, Executed }
struct Transaction {
address initiator;
uint amount;
State state;
}
mapping(uint => Transaction) public transactions;
uint public transactionCount;
function initiateTransaction(uint amount) public {
transactions[transactionCount] = Transaction(msg.sender, amount, State.Initiated);
transactionCount++;
}
function approveTransaction(uint id) public {
require(transactions[id].state == State.Initiated, "Not in initiated state");
transactions[id].state = State.Approved;
}
function executeTransaction(uint id) public {
require(transactions[id].state == State.Approved, "Not approved");
transactions[id].state = State.Executed;
}
}
In this contract:
Initiated, Approved, and Executed.module MULTI-STEP-APPROVAL
imports INT
imports MAP
imports BOOL
syntax ApprovalAction ::= "initiateTransaction" | "approveTransaction" | "executeTransaction"
syntax Address ::= String
syntax ApprovalState ::= Map
syntax KResult ::= Int
configuration <k> $PGM:K </k>
<transactions> .Map </transactions>
// Rule for initiateTransaction function
rule <k> initiateTransaction(AMOUNT) => . ... </k>
<transactions> TS => TS[TX_ID <- { initiator: INITIATOR, amount: AMOUNT, state: "Initiated" }] </transactions>
// Rule for approveTransaction function
rule <k> approveTransaction(TX_ID) => . ... </k>
<transactions> TS => TS[TX_ID <- { state: "Approved" }] </transactions>
requires TS[TX_ID].state == "Initiated"
// Rule for executeTransaction function
rule <k> executeTransaction(TX_ID) => . ... </k>
<transactions> TS => TS[TX_ID <- { state: "Executed" }] </transactions>
requires TS[TX_ID].state == "Approved"
In this K specification:
This contract introduces ownership transfer where only the current owner can transfer ownership to another address.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;
contract Ownable {
address public owner;
constructor() {
owner = msg.sender;
}
modifier onlyOwner() {
require(msg.sender == owner, "Not the owner");
_;
}
function transferOwnership(address newOwner) public onlyOwner {
require(newOwner != address(0), "New owner is zero address");
owner = newOwner;
}
}
In this contract:
transferOwnership.module OWNABLE
imports BOOL
imports STRING
syntax OwnershipAction ::= "transferOwnership"
syntax Address ::= String
configuration <k> $PGM:K </k>
<owner> .String </owner>
// Rule for transferOwnership function
rule <k> transferOwnership(NEW_OWNER) => . ... </k>
<owner> _ => NEW_OWNER </owner>
requires SENDER == OWNER andBool NEW_OWNER =/=K "0x0"
In this K specification:
transferOwnership rule verifies that the sender is the current owner and the new owner address is not zero.This example is an escrow contract where an arbiter manages the funds and can release them to a recipient.
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.0;
contract Escrow {
address public payer;
address public recipient;
address public arbiter;
constructor(address _recipient, address _arbiter) payable {
payer = msg.sender;
recipient = _recipient;
arbiter = _arbiter;
}
function releaseFunds() public {
require(msg.sender == arbiter, "Only arbiter can release funds");
payable(recipient).transfer(address(this).balance);
}
}
In this contract:
module ESCROW
imports BOOL
imports INT
imports STRING
syntax EscrowAction ::= "releaseFunds"
syntax Address ::= String
configuration <k> $PGM:K </k>
<balance> 0 </balance>
<arbiter> .String </arbiter>
<recipient> .String </recipient>
// Rule for releaseFunds function
rule <k> releaseFunds => . ... </k>
<balance> BAL => 0 </balance>
requires SENDER == ARBITER andBool BAL >Int 0
In this K specification:
releaseFunds rule checks that only the arbiter can release funds and that there are funds to release.